The present invention relates to a logical verification of a circuit. More particularly, this invention relates to logic verification method and apparatus.
In the case of a circuit for which circuit information (net list) is arranged hierarchically is changed, although the whole circuit is equivalent logically, input ports may increase and the logic maybe inverted occasionally in a low-hierarchical block.
For example, FIG. 8 is a block diagram showing a conventional logic verification method disclosed in Japanese Patent Application Laid-Open No. 9-146991. With reference to FIG. 8, a corresponding relationship extraction unit 1100 extracts a corresponding relationship of output ports from a low-hierarchical block or input ports to the low-hierarchical block in a logic circuit before and after changing a circuit (hereinafter, old logic circuit and new logic circuit).
Further, a logic function calculation unit 1200 calculates a logic function of the input ports or output ports in the old and new logic circuits. A logic verification unit 1300 judges logic equivalence in the input ports of the old and new logic circuits according to the corresponding relationship extracted by the corresponding relationship extraction unit 1100.
In addition, in the case where the logic functions of the input ports in the old and new logic circuits are different from each other, as the result of the judgment in the logic verification unit 1300, an error backward propagation unit 1400 makes calculations from the input port in the old logic circuit to the backward side so as to be equivalent to the logic functions of the input ports in the new logic circuit.
A correcting portion determination unit 1500 determines a correcting portion of the old logic circuit based on the calculated result in the error backward propagation unit 1400. A specification function implementation unit 1600 implements a specification function of the correcting portion. A storage unit 1700 stores a portion which is not corrected in the old logic circuit.
When the logic equivalence is verified by using a logic verification method where the old and new logic circuits which have been changed logically can be realized hierarchically, the number of the input ports in the low-hierarchical blocks and the logic in the input ports are different. As a result, correct comparison cannot be made.
One aspect of the invention provides logic verification method and apparatus which make a logic verification in a low-hierarchical block, make a logic verification in a high-hierarchical circuit in a state that the low-hierarchical block is not subject of comparison, and even if a number of comparison points in the low-hierarchical block increases due to the change of the circuit, verify logical equivalence in the high-hierarchical circuit using equivalence information of the comparison points in the method of verifying logical equivalence before and after a change of a circuit in which circuit information is composed hierarchically.
Further, another aspect of the invention provides a logic verification method, of verifying logical equivalence before and after a change of a circuit in which circuit information is composed hierarchically, which includes the steps of: judging that a number of input ports in first and second low-hierarchical blocks is different and recognizing that a second input port in the second low-hierarchical block is left; executing backward retrieval from the second input port in the second low-hierarchical block based on the circuit information until a branch point is found; finding the branch point as a result of the backward retrieval; when the branch point is found, executing forward retrieval from the branch point; finding a first input port in the second low-hierarchical block as a result of the forward retrieval; judging as to whether or not the first and second input port in the second low-hierarchical block are equivalent logically to each other using circuit information of the first and second input ports in the second low-hierarchical block; when first and second ports are equivalent logically, regarding that the first and second input ports in the second low-hierarchical block are equal to each other; and when the first and second ports are not equivalent logically, returning to the step of executing the forward retrieval from the branch point.
Further, still another aspect of the invention provides a logic verification method, of verifying logical equivalence before and after a change of a circuit in which circuit information is composed hierarchically, which includes the steps of: when non-equivalence occurs at first comparison points in first and second low-hierarchical blocks, analyzing the non-equivalence at the first comparison points in the first and second low-hierarchical blocks; finding second comparison points in the first and second low-hierarchical blocks as a cause of the non-equivalence; inverting the second comparison points in the first and second low-hierarchical blocks so as to again compare logic of the first comparison points in the first and second low-hierarchical blocks; judging as to whether or not the logic is equivalent at the first comparison points in the first and second low-hierarchical blocks; when the logic is not equivalent, regarding the non-equivalence at the first comparison points in the first and second low-hierarchical blocks as true non-equivalence; when the logic is equivalent, creating information that second comparison points in the first and second low-hierarchical blocks establish an inverted relationship so as to compare logic in high-hierarchical block or another equal-hierarchical block at the second points in the first and second low-hierarchical blocks using the information; judging as to whether or not the logic is equivalent at the second comparison points in the first and second low-hierarchical blocks; when the logic is not equivalent, regarding the non-equivalence at the second comparison points in the first and second low-hierarchical blocks as true non-equivalence; and when the logic is equivalent, regarding the non-equivalence at the second comparison points in the first and second low-hierarchical blocks as false non-equivalence.
Further, still another aspect of the invention provides a logic verification method, of verifying logical equivalence before and after a change of a circuit in which circuit information is composed hierarchically, which includes the steps of: when non-equivalence occurs at first comparison points in first and second equal-hierarchical blocks, inverting the first comparison points in the first and second equal-hierarchical blocks so as to make a comparison; judging as to whether or not logic is equivalent at the first comparison points in the first and second equal-hierarchical blocks; when the logic is not equivalent, regarding the non-equivalence at the first comparison points in the first and second equal-hierarchical blocks as true non-equivalence; when the logic is equivalent, comparing second comparison points in the first and second equal-hierarchical blocks; judging as to whether or not the logic is equivalent at the second comparison points in the first and second equal-hierarchical blocks; when the logic is not equivalent, again comparing logic at the second comparison points in the first and second equal-hierarchical blocks using a condition that the first comparison point in the first equal-hierarchical block is not the first comparison point in the second equal-hierarchical block; when the logic is equivalent, regarding the non-equivalence at the first comparison points in the first and second equal-hierarchical blocks as true non-equivalence; judging as to whether or not logic is equivalent at the second comparison points in the first and second equal-hierarchical blocks; when the logic is not equivalent, regarding the non-equivalence at the first comparison points in the first and second equal-hierarchical blocks as true non-equivalence; and when the logic is equivalent, regarding the non-equivalence at the first comparison points in the first and second equal-hierarchical blocks as false non-equivalence.
Further, still another aspect of the invention provides a logic verification apparatus, for verifying logical equivalence before and after a change of a circuit in which circuit information is composed hierarchically, which includes means for making a logic verification in a low-hierarchical block, making a logic verification in a high-hierarchical circuit in a state that the low-hierarchical block is not the subject of comparison, and even if a number of comparison points in the low-hierarchical block increases due to the change of the circuit, verifying logical equivalence in the high-hierarchical circuit using equivalence information of the comparison points.
Further, still another aspect of the invention provides a logic verification apparatus, for verifying logical equivalence before and after a change of a circuit in which circuit information is composed hierarchically, which includes means for making a verification by means of the logic verification method according to any one of the above-mentioned aspects.
Other objects and features of this invention will become apparent from the following description with reference to the accompanying drawings.